Termination w.r.t. Q proof of /tmp/aprove_benchmark_example

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

FACT(ok(X)) → FACT(X)
ACTIVE(add(X1, X2)) → ACTIVE(X1)
PROPER(add(X1, X2)) → ADD(proper(X1), proper(X2))
ACTIVE(prod(s(X), Y)) → ADD(Y, prod(X, Y))
PROPER(if(X1, X2, X3)) → PROPER(X1)
ADD(mark(X1), X2) → ADD(X1, X2)
PROPER(add(X1, X2)) → PROPER(X2)
ACTIVE(prod(s(X), Y)) → PROD(X, Y)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)
ACTIVE(if(X1, X2, X3)) → IF(active(X1), X2, X3)
ACTIVE(p(X)) → P(active(X))
ACTIVE(zero(X)) → ACTIVE(X)
ADD(ok(X1), ok(X2)) → ADD(X1, X2)
ACTIVE(add(X1, X2)) → ADD(active(X1), X2)
PROPER(prod(X1, X2)) → PROPER(X2)
PROPER(zero(X)) → ZERO(proper(X))
PROPER(fact(X)) → FACT(proper(X))
PROPER(s(X)) → S(proper(X))
ACTIVE(prod(X1, X2)) → PROD(active(X1), X2)
P(ok(X)) → P(X)
PROPER(fact(X)) → PROPER(X)
ACTIVE(fact(X)) → P(X)
ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(p(X)) → ACTIVE(X)
S(ok(X)) → S(X)
PROPER(zero(X)) → PROPER(X)
PROPER(p(X)) → PROPER(X)
ACTIVE(add(s(X), Y)) → ADD(X, Y)
TOP(mark(X)) → PROPER(X)
ACTIVE(add(s(X), Y)) → S(add(X, Y))
PROD(X1, mark(X2)) → PROD(X1, X2)
FACT(mark(X)) → FACT(X)
P(mark(X)) → P(X)
PROPER(add(X1, X2)) → PROPER(X1)
ACTIVE(fact(X)) → ACTIVE(X)
ACTIVE(prod(X1, X2)) → PROD(X1, active(X2))
PROD(mark(X1), X2) → PROD(X1, X2)
ADD(X1, mark(X2)) → ADD(X1, X2)
TOP(ok(X)) → ACTIVE(X)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → IF(proper(X1), proper(X2), proper(X3))
PROPER(if(X1, X2, X3)) → PROPER(X3)
ACTIVE(fact(X)) → FACT(p(X))
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
TOP(ok(X)) → TOP(active(X))
ACTIVE(zero(X)) → ZERO(active(X))
ACTIVE(fact(X)) → PROD(X, fact(p(X)))
PROD(ok(X1), ok(X2)) → PROD(X1, X2)
S(mark(X)) → S(X)
ACTIVE(prod(X1, X2)) → ACTIVE(X1)
ACTIVE(fact(X)) → ZERO(X)
PROPER(if(X1, X2, X3)) → PROPER(X2)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
ACTIVE(add(X1, X2)) → ACTIVE(X2)
ACTIVE(prod(X1, X2)) → ACTIVE(X2)
PROPER(prod(X1, X2)) → PROPER(X1)
ACTIVE(fact(X)) → S(0)
PROPER(p(X)) → P(proper(X))
ZERO(ok(X)) → ZERO(X)
TOP(mark(X)) → TOP(proper(X))
ACTIVE(add(X1, X2)) → ADD(X1, active(X2))
PROPER(prod(X1, X2)) → PROD(proper(X1), proper(X2))
ZERO(mark(X)) → ZERO(X)
ACTIVE(fact(X)) → FACT(active(X))
ACTIVE(fact(X)) → IF(zero(X), s(0), prod(X, fact(p(X))))
ACTIVE(s(X)) → S(active(X))

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

FACT(ok(X)) → FACT(X)
ACTIVE(add(X1, X2)) → ACTIVE(X1)
PROPER(add(X1, X2)) → ADD(proper(X1), proper(X2))
ACTIVE(prod(s(X), Y)) → ADD(Y, prod(X, Y))
PROPER(if(X1, X2, X3)) → PROPER(X1)
ADD(mark(X1), X2) → ADD(X1, X2)
PROPER(add(X1, X2)) → PROPER(X2)
ACTIVE(prod(s(X), Y)) → PROD(X, Y)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)
ACTIVE(if(X1, X2, X3)) → IF(active(X1), X2, X3)
ACTIVE(p(X)) → P(active(X))
ACTIVE(zero(X)) → ACTIVE(X)
ADD(ok(X1), ok(X2)) → ADD(X1, X2)
ACTIVE(add(X1, X2)) → ADD(active(X1), X2)
PROPER(prod(X1, X2)) → PROPER(X2)
PROPER(zero(X)) → ZERO(proper(X))
PROPER(fact(X)) → FACT(proper(X))
PROPER(s(X)) → S(proper(X))
ACTIVE(prod(X1, X2)) → PROD(active(X1), X2)
P(ok(X)) → P(X)
PROPER(fact(X)) → PROPER(X)
ACTIVE(fact(X)) → P(X)
ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(p(X)) → ACTIVE(X)
S(ok(X)) → S(X)
PROPER(zero(X)) → PROPER(X)
PROPER(p(X)) → PROPER(X)
ACTIVE(add(s(X), Y)) → ADD(X, Y)
TOP(mark(X)) → PROPER(X)
ACTIVE(add(s(X), Y)) → S(add(X, Y))
PROD(X1, mark(X2)) → PROD(X1, X2)
FACT(mark(X)) → FACT(X)
P(mark(X)) → P(X)
PROPER(add(X1, X2)) → PROPER(X1)
ACTIVE(fact(X)) → ACTIVE(X)
ACTIVE(prod(X1, X2)) → PROD(X1, active(X2))
PROD(mark(X1), X2) → PROD(X1, X2)
ADD(X1, mark(X2)) → ADD(X1, X2)
TOP(ok(X)) → ACTIVE(X)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → IF(proper(X1), proper(X2), proper(X3))
PROPER(if(X1, X2, X3)) → PROPER(X3)
ACTIVE(fact(X)) → FACT(p(X))
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
TOP(ok(X)) → TOP(active(X))
ACTIVE(zero(X)) → ZERO(active(X))
ACTIVE(fact(X)) → PROD(X, fact(p(X)))
PROD(ok(X1), ok(X2)) → PROD(X1, X2)
S(mark(X)) → S(X)
ACTIVE(prod(X1, X2)) → ACTIVE(X1)
ACTIVE(fact(X)) → ZERO(X)
PROPER(if(X1, X2, X3)) → PROPER(X2)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
ACTIVE(add(X1, X2)) → ACTIVE(X2)
ACTIVE(prod(X1, X2)) → ACTIVE(X2)
PROPER(prod(X1, X2)) → PROPER(X1)
ACTIVE(fact(X)) → S(0)
PROPER(p(X)) → P(proper(X))
ZERO(ok(X)) → ZERO(X)
TOP(mark(X)) → TOP(proper(X))
ACTIVE(add(X1, X2)) → ADD(X1, active(X2))
PROPER(prod(X1, X2)) → PROD(proper(X1), proper(X2))
ZERO(mark(X)) → ZERO(X)
ACTIVE(fact(X)) → FACT(active(X))
ACTIVE(fact(X)) → IF(zero(X), s(0), prod(X, fact(p(X))))
ACTIVE(s(X)) → S(active(X))

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 10 SCCs with 28 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ADD(ok(X1), ok(X2)) → ADD(X1, X2)
ADD(X1, mark(X2)) → ADD(X1, X2)
ADD(mark(X1), X2) → ADD(X1, X2)

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ADD(ok(X1), ok(X2)) → ADD(X1, X2)
ADD(X1, mark(X2)) → ADD(X1, X2)
ADD(mark(X1), X2) → ADD(X1, X2)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ADD(ok(X1), ok(X2)) → ADD(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
ADD(X1, mark(X2)) → ADD(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
ADD(mark(X1), X2) → ADD(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(mark(X)) → P(X)
P(ok(X)) → P(X)

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P(mark(X)) → P(X)
P(ok(X)) → P(X)

From the DPs we obtained the following set of size-change graphs:

P(mark(X)) → P(X)
The graph contains the following edges 1 > 1
P(ok(X)) → P(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROD(ok(X1), ok(X2)) → PROD(X1, X2)
PROD(X1, mark(X2)) → PROD(X1, X2)
PROD(mark(X1), X2) → PROD(X1, X2)

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROD(ok(X1), ok(X2)) → PROD(X1, X2)
PROD(X1, mark(X2)) → PROD(X1, X2)
PROD(mark(X1), X2) → PROD(X1, X2)

From the DPs we obtained the following set of size-change graphs:

PROD(ok(X1), ok(X2)) → PROD(X1, X2)
The graph contains the following edges 1 > 1, 2 > 2
PROD(X1, mark(X2)) → PROD(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
PROD(mark(X1), X2) → PROD(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(ok(X)) → S(X)
S(mark(X)) → S(X)

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(ok(X)) → S(X)
S(mark(X)) → S(X)

From the DPs we obtained the following set of size-change graphs:

S(ok(X)) → S(X)
The graph contains the following edges 1 > 1
S(mark(X)) → S(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ZERO(ok(X)) → ZERO(X)
ZERO(mark(X)) → ZERO(X)

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ZERO(ok(X)) → ZERO(X)
ZERO(mark(X)) → ZERO(X)

From the DPs we obtained the following set of size-change graphs:

ZERO(ok(X)) → ZERO(X)
The graph contains the following edges 1 > 1
ZERO(mark(X)) → ZERO(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)

From the DPs we obtained the following set of size-change graphs:

IF(mark(X1), X2, X3) → IF(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
IF(ok(X1), ok(X2), ok(X3)) → IF(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FACT(ok(X)) → FACT(X)
FACT(mark(X)) → FACT(X)

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FACT(ok(X)) → FACT(X)
FACT(mark(X)) → FACT(X)

From the DPs we obtained the following set of size-change graphs:

FACT(ok(X)) → FACT(X)
The graph contains the following edges 1 > 1
FACT(mark(X)) → FACT(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROPER(zero(X)) → PROPER(X)
PROPER(p(X)) → PROPER(X)
PROPER(s(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → PROPER(X2)
PROPER(fact(X)) → PROPER(X)
PROPER(add(X1, X2)) → PROPER(X2)
PROPER(prod(X1, X2)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X3)
PROPER(add(X1, X2)) → PROPER(X1)
PROPER(if(X1, X2, X3)) → PROPER(X1)
PROPER(prod(X1, X2)) → PROPER(X1)

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROPER(zero(X)) → PROPER(X)
PROPER(p(X)) → PROPER(X)
PROPER(fact(X)) → PROPER(X)
PROPER(if(X1, X2, X3)) → PROPER(X2)
PROPER(s(X)) → PROPER(X)
PROPER(prod(X1, X2)) → PROPER(X2)
PROPER(add(X1, X2)) → PROPER(X2)
PROPER(if(X1, X2, X3)) → PROPER(X3)
PROPER(add(X1, X2)) → PROPER(X1)
PROPER(if(X1, X2, X3)) → PROPER(X1)
PROPER(prod(X1, X2)) → PROPER(X1)

From the DPs we obtained the following set of size-change graphs:

PROPER(zero(X)) → PROPER(X)
The graph contains the following edges 1 > 1
PROPER(p(X)) → PROPER(X)
The graph contains the following edges 1 > 1
PROPER(s(X)) → PROPER(X)
The graph contains the following edges 1 > 1
PROPER(if(X1, X2, X3)) → PROPER(X2)
The graph contains the following edges 1 > 1
PROPER(fact(X)) → PROPER(X)
The graph contains the following edges 1 > 1
PROPER(add(X1, X2)) → PROPER(X2)
The graph contains the following edges 1 > 1
PROPER(prod(X1, X2)) → PROPER(X2)
The graph contains the following edges 1 > 1
PROPER(if(X1, X2, X3)) → PROPER(X3)
The graph contains the following edges 1 > 1
PROPER(add(X1, X2)) → PROPER(X1)
The graph contains the following edges 1 > 1
PROPER(if(X1, X2, X3)) → PROPER(X1)
The graph contains the following edges 1 > 1
PROPER(prod(X1, X2)) → PROPER(X1)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(zero(X)) → ACTIVE(X)
ACTIVE(add(X1, X2)) → ACTIVE(X1)
ACTIVE(prod(X1, X2)) → ACTIVE(X1)
ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(add(X1, X2)) → ACTIVE(X2)
ACTIVE(fact(X)) → ACTIVE(X)
ACTIVE(prod(X1, X2)) → ACTIVE(X2)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(p(X)) → ACTIVE(X)

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(zero(X)) → ACTIVE(X)
ACTIVE(prod(X1, X2)) → ACTIVE(X1)
ACTIVE(add(X1, X2)) → ACTIVE(X1)
ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(fact(X)) → ACTIVE(X)
ACTIVE(add(X1, X2)) → ACTIVE(X2)
ACTIVE(prod(X1, X2)) → ACTIVE(X2)
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(p(X)) → ACTIVE(X)

From the DPs we obtained the following set of size-change graphs:

ACTIVE(zero(X)) → ACTIVE(X)
The graph contains the following edges 1 > 1
ACTIVE(add(X1, X2)) → ACTIVE(X1)
The graph contains the following edges 1 > 1
ACTIVE(prod(X1, X2)) → ACTIVE(X1)
The graph contains the following edges 1 > 1
ACTIVE(s(X)) → ACTIVE(X)
The graph contains the following edges 1 > 1
ACTIVE(add(X1, X2)) → ACTIVE(X2)
The graph contains the following edges 1 > 1
ACTIVE(fact(X)) → ACTIVE(X)
The graph contains the following edges 1 > 1
ACTIVE(prod(X1, X2)) → ACTIVE(X2)
The graph contains the following edges 1 > 1
ACTIVE(if(X1, X2, X3)) → ACTIVE(X1)
The graph contains the following edges 1 > 1
ACTIVE(p(X)) → ACTIVE(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

Q DP problem:
The TRS P consists of the following rules:

TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))
fact(mark(X)) → mark(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
s(mark(X)) → mark(s(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
p(mark(X)) → mark(p(X))
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
fact(ok(X)) → ok(fact(X))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(ok(X)) → ok(zero(X))
s(ok(X)) → ok(s(X))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0
POL(TOP(x₁)) = x₁
POL(active(x₁)) = 2·x₁
POL(add(x₁, x₂)) = x₁ + x₂
POL(fact(x₁)) = 2·x₁
POL(false) = 0
POL(if(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(mark(x₁)) = x₁
POL(ok(x₁)) = 2·x₁
POL(p(x₁)) = x₁
POL(prod(x₁, x₂)) = x₁ + x₂
POL(proper(x₁)) = x₁
POL(s(x₁)) = 2·x₁
POL(true) = 0
POL(zero(x₁)) = x₁

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(mark(X)) → TOP(proper(X)) at position [0] we obtained the following new rules:

TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(true)) → TOP(ok(true))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))
TOP(mark(false)) → TOP(ok(false))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(p(x0))) → TOP(p(proper(x0)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(mark(true)) → TOP(ok(true))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(false)) → TOP(ok(false))
TOP(ok(X)) → TOP(active(X))

The TRS R consists of the following rules:

proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule TOP(ok(X)) → TOP(active(X)) at position [0] we obtained the following new rules:

TOP(ok(zero(x0))) → TOP(zero(active(x0)))
TOP(ok(add(0, x0))) → TOP(mark(x0))
TOP(ok(prod(x0, x1))) → TOP(prod(active(x0), x1))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(ok(zero(s(x0)))) → TOP(mark(false))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(add(s(x0), x1))) → TOP(mark(s(add(x0, x1))))
TOP(ok(prod(s(x0), x1))) → TOP(mark(add(x1, prod(x0, x1))))
TOP(ok(prod(0, x0))) → TOP(mark(0))
TOP(ok(zero(0))) → TOP(mark(true))
TOP(ok(fact(x0))) → TOP(mark(if(zero(x0), s(0), prod(x0, fact(p(x0))))))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(x0, active(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(fact(x0))) → TOP(fact(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(active(x0), x1))
TOP(ok(prod(x0, x1))) → TOP(prod(x0, active(x1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(add(0, x0))) → TOP(mark(x0))
TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(add(s(x0), x1))) → TOP(mark(s(add(x0, x1))))
TOP(ok(prod(0, x0))) → TOP(mark(0))
TOP(ok(zero(0))) → TOP(mark(true))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(add(x0, x1))) → TOP(add(x0, active(x1)))
TOP(ok(fact(x0))) → TOP(fact(active(x0)))
TOP(mark(true)) → TOP(ok(true))
TOP(ok(add(x0, x1))) → TOP(add(active(x0), x1))
TOP(ok(prod(x0, x1))) → TOP(prod(x0, active(x1)))
TOP(ok(zero(x0))) → TOP(zero(active(x0)))
TOP(ok(prod(x0, x1))) → TOP(prod(active(x0), x1))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(zero(s(x0)))) → TOP(mark(false))
TOP(ok(prod(s(x0), x1))) → TOP(mark(add(x1, prod(x0, x1))))
TOP(mark(false)) → TOP(ok(false))
TOP(mark(0)) → TOP(ok(0))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(fact(x0))) → TOP(mark(if(zero(x0), s(0), prod(x0, fact(p(x0))))))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))

The TRS R consists of the following rules:

proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(zero(x0))) → TOP(zero(active(x0)))
TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(ok(add(0, x0))) → TOP(mark(x0))
TOP(ok(prod(x0, x1))) → TOP(prod(active(x0), x1))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(add(s(x0), x1))) → TOP(mark(s(add(x0, x1))))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(prod(s(x0), x1))) → TOP(mark(add(x1, prod(x0, x1))))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(fact(x0))) → TOP(mark(if(zero(x0), s(0), prod(x0, fact(p(x0))))))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(x0, active(x1)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(ok(fact(x0))) → TOP(fact(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(active(x0), x1))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))
TOP(ok(prod(x0, x1))) → TOP(prod(x0, active(x1)))

The TRS R consists of the following rules:

proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

TOP(ok(fact(x0))) → TOP(mark(if(zero(x0), s(0), prod(x0, fact(p(x0))))))

The remaining pairs can at least be oriented weakly.

TOP(ok(zero(x0))) → TOP(zero(active(x0)))
TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(ok(add(0, x0))) → TOP(mark(x0))
TOP(ok(prod(x0, x1))) → TOP(prod(active(x0), x1))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(add(s(x0), x1))) → TOP(mark(s(add(x0, x1))))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(prod(s(x0), x1))) → TOP(mark(add(x1, prod(x0, x1))))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(x0, active(x1)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(ok(fact(x0))) → TOP(fact(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(active(x0), x1))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))
TOP(ok(prod(x0, x1))) → TOP(prod(x0, active(x1)))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(TOP(x₁)) = x₁
POL(active(x₁)) = x₁
POL(add(x₁, x₂)) = x₂
POL(fact(x₁)) = 1 + x₁
POL(false) = 0
POL(if(x₁, x₂, x₃)) = x₂ + x₃
POL(mark(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(p(x₁)) = x₁
POL(prod(x₁, x₂)) = 0
POL(proper(x₁)) = x₁
POL(s(x₁)) = x₁
POL(true) = 0
POL(zero(x₁)) = 0

The following usable rules [17] were oriented:

active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(add(X1, X2)) → add(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
p(mark(X)) → mark(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(mark(X1), X2) → mark(add(X1, X2))
proper(false) → ok(false)
proper(true) → ok(true)
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(zero(X)) → zero(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(fact(X)) → fact(proper(X))
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(zero(x0))) → TOP(zero(active(x0)))
TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(ok(add(0, x0))) → TOP(mark(x0))
TOP(ok(prod(x0, x1))) → TOP(prod(active(x0), x1))
TOP(ok(p(s(x0)))) → TOP(mark(x0))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(add(s(x0), x1))) → TOP(mark(s(add(x0, x1))))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(prod(s(x0), x1))) → TOP(mark(add(x1, prod(x0, x1))))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(ok(add(x0, x1))) → TOP(add(x0, active(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(fact(x0))) → TOP(fact(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(active(x0), x1))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))
TOP(ok(prod(x0, x1))) → TOP(prod(x0, active(x1)))

The TRS R consists of the following rules:

proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

TOP(ok(p(s(x0)))) → TOP(mark(x0))

The remaining pairs can at least be oriented weakly.

TOP(ok(zero(x0))) → TOP(zero(active(x0)))
TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(ok(add(0, x0))) → TOP(mark(x0))
TOP(ok(prod(x0, x1))) → TOP(prod(active(x0), x1))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(add(s(x0), x1))) → TOP(mark(s(add(x0, x1))))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(prod(s(x0), x1))) → TOP(mark(add(x1, prod(x0, x1))))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(ok(add(x0, x1))) → TOP(add(x0, active(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(fact(x0))) → TOP(fact(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(active(x0), x1))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))
TOP(ok(prod(x0, x1))) → TOP(prod(x0, active(x1)))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(TOP(x₁)) = x₁
POL(active(x₁)) = x₁
POL(add(x₁, x₂)) = x₂
POL(fact(x₁)) = 1
POL(false) = 0
POL(if(x₁, x₂, x₃)) = x₂ + x₃
POL(mark(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(p(x₁)) = 1 + x₁
POL(prod(x₁, x₂)) = 0
POL(proper(x₁)) = x₁
POL(s(x₁)) = x₁
POL(true) = 0
POL(zero(x₁)) = 0

The following usable rules [17] were oriented:

active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(add(X1, X2)) → add(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
p(mark(X)) → mark(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(mark(X1), X2) → mark(add(X1, X2))
proper(false) → ok(false)
proper(true) → ok(true)
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(zero(X)) → zero(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(fact(X)) → fact(proper(X))
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(zero(x0))) → TOP(zero(active(x0)))
TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(ok(add(0, x0))) → TOP(mark(x0))
TOP(ok(prod(x0, x1))) → TOP(prod(active(x0), x1))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(add(s(x0), x1))) → TOP(mark(s(add(x0, x1))))
TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(prod(s(x0), x1))) → TOP(mark(add(x1, prod(x0, x1))))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(x0, active(x1)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(ok(fact(x0))) → TOP(fact(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(active(x0), x1))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))
TOP(ok(prod(x0, x1))) → TOP(prod(x0, active(x1)))

The TRS R consists of the following rules:

proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

TOP(ok(if(false, x0, x1))) → TOP(mark(x1))
TOP(ok(if(true, x0, x1))) → TOP(mark(x0))

The remaining pairs can at least be oriented weakly.

TOP(ok(zero(x0))) → TOP(zero(active(x0)))
TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(ok(add(0, x0))) → TOP(mark(x0))
TOP(ok(prod(x0, x1))) → TOP(prod(active(x0), x1))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(add(s(x0), x1))) → TOP(mark(s(add(x0, x1))))
TOP(ok(prod(s(x0), x1))) → TOP(mark(add(x1, prod(x0, x1))))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(x0, active(x1)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(ok(fact(x0))) → TOP(fact(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(active(x0), x1))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))
TOP(ok(prod(x0, x1))) → TOP(prod(x0, active(x1)))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(TOP(x₁)) = x₁
POL(active(x₁)) = x₁
POL(add(x₁, x₂)) = x₂
POL(fact(x₁)) = 1
POL(false) = 0
POL(if(x₁, x₂, x₃)) = 1 + x₂ + x₃
POL(mark(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(p(x₁)) = x₁
POL(prod(x₁, x₂)) = 0
POL(proper(x₁)) = x₁
POL(s(x₁)) = x₁
POL(true) = 0
POL(zero(x₁)) = 0

The following usable rules [17] were oriented:

active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(add(X1, X2)) → add(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
p(mark(X)) → mark(p(X))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(mark(X1), X2) → mark(add(X1, X2))
proper(false) → ok(false)
proper(true) → ok(true)
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(zero(X)) → zero(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(fact(X)) → fact(proper(X))
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesReductionPairsProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ QDPOrderProof

                                  ↳ QDP

                                    ↳ QDPOrderProof

                                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TOP(ok(zero(x0))) → TOP(zero(active(x0)))
TOP(mark(zero(x0))) → TOP(zero(proper(x0)))
TOP(ok(add(0, x0))) → TOP(mark(x0))
TOP(ok(prod(x0, x1))) → TOP(prod(active(x0), x1))
TOP(mark(s(x0))) → TOP(s(proper(x0)))
TOP(ok(if(x0, x1, x2))) → TOP(if(active(x0), x1, x2))
TOP(ok(add(s(x0), x1))) → TOP(mark(s(add(x0, x1))))
TOP(ok(prod(s(x0), x1))) → TOP(mark(add(x1, prod(x0, x1))))
TOP(mark(p(x0))) → TOP(p(proper(x0)))
TOP(ok(s(x0))) → TOP(s(active(x0)))
TOP(mark(prod(x0, x1))) → TOP(prod(proper(x0), proper(x1)))
TOP(mark(if(x0, x1, x2))) → TOP(if(proper(x0), proper(x1), proper(x2)))
TOP(mark(fact(x0))) → TOP(fact(proper(x0)))
TOP(ok(add(x0, x1))) → TOP(add(x0, active(x1)))
TOP(ok(p(x0))) → TOP(p(active(x0)))
TOP(ok(fact(x0))) → TOP(fact(active(x0)))
TOP(ok(add(x0, x1))) → TOP(add(active(x0), x1))
TOP(mark(add(x0, x1))) → TOP(add(proper(x0), proper(x1)))
TOP(ok(prod(x0, x1))) → TOP(prod(x0, active(x1)))

The TRS R consists of the following rules:

proper(fact(X)) → fact(proper(X))
proper(if(X1, X2, X3)) → if(proper(X1), proper(X2), proper(X3))
proper(zero(X)) → zero(proper(X))
proper(s(X)) → s(proper(X))
proper(0) → ok(0)
proper(prod(X1, X2)) → prod(proper(X1), proper(X2))
proper(p(X)) → p(proper(X))
proper(add(X1, X2)) → add(proper(X1), proper(X2))
proper(true) → ok(true)
proper(false) → ok(false)
add(mark(X1), X2) → mark(add(X1, X2))
add(X1, mark(X2)) → mark(add(X1, X2))
add(ok(X1), ok(X2)) → ok(add(X1, X2))
p(mark(X)) → mark(p(X))
p(ok(X)) → ok(p(X))
prod(mark(X1), X2) → mark(prod(X1, X2))
prod(X1, mark(X2)) → mark(prod(X1, X2))
prod(ok(X1), ok(X2)) → ok(prod(X1, X2))
s(mark(X)) → mark(s(X))
s(ok(X)) → ok(s(X))
zero(mark(X)) → mark(zero(X))
zero(ok(X)) → ok(zero(X))
if(mark(X1), X2, X3) → mark(if(X1, X2, X3))
if(ok(X1), ok(X2), ok(X3)) → ok(if(X1, X2, X3))
fact(mark(X)) → mark(fact(X))
fact(ok(X)) → ok(fact(X))
active(fact(X)) → mark(if(zero(X), s(0), prod(X, fact(p(X)))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(prod(0, X)) → mark(0)
active(prod(s(X), Y)) → mark(add(Y, prod(X, Y)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
active(zero(0)) → mark(true)
active(zero(s(X))) → mark(false)
active(p(s(X))) → mark(X)
active(fact(X)) → fact(active(X))
active(if(X1, X2, X3)) → if(active(X1), X2, X3)
active(zero(X)) → zero(active(X))
active(s(X)) → s(active(X))
active(prod(X1, X2)) → prod(active(X1), X2)
active(prod(X1, X2)) → prod(X1, active(X2))
active(p(X)) → p(active(X))
active(add(X1, X2)) → add(active(X1), X2)
active(add(X1, X2)) → add(X1, active(X2))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.